\begin{nusmvCommand}{check\_ltlspec} {Performs LTL model checking}

\cmdLine{check\_ltlspec [-h] [-m | -o output-file] [-n number | -p \linebreak"\ltlexpr [IN context]"]}

Performs model checking of LTL formulas. LTL model checking is reduced
to CTL model checking as described in the paper by \cite{CGH97}.

A \ltlexpr to be checked can be specified at command line
using option  \commandopt{p}. Alternatively, option \commandopt{n} can be used
for checking a particular formula in the property database. If neither
\commandopt{n} nor \commandopt{p} are used, all the LTLSPEC formulas in the
database are checked.

\begin{cmdOpt}
\opt{-m}{ Pipes the output generated by the command in processing
\code{LTLSPEC}{s} to the program specified by the \shellvar{PAGER} shell
variable if defined, else through the \unix command \shellcommand{more}.}

\opt{-o \parameter{\filename{output-file}}}{ Writes the output generated by the command in
processing \code{LTLSPEC}{s} to the file \filename{output-file}.}

\opt{-p \parameter{"\ltlexpr [IN context]"}}{ An LTL formula to be checked.
\code{context} is the module instance name which the variables in
\ltlexpr must be evaluated in.}
  
\opt{-n \parameter{\natnum{number}}}{ Checks the LTL property with index \natnum{number} in
the property database.}

\end{cmdOpt}

\end{nusmvCommand}
